In recent years, a verification method based on a model checking is known as a verification method of a system and software. The model checking is a technique for verifying whether a verification target satisfies a specification by making a verification target into a model as a state transition system and exhaustively searching the model. The model checking can be applied from a design stage, and can guarantee whether the verification target satisfies the specification or not, and therefore, the model checking attracts attention as a technique for improving the reliability of the system and the software.
Recently, an attempt is made to apply the model checking to verification of a network. For example, NPL 1 discloses a technique in which, when a state search of a network controlled by a technique called OpenFlow (see NPLs 2, 3) is performed with the model checking, a program of an OpenFlow controller is symbolically executed, and a set of representing values of packets for executing all the code paths is derived, and the state search is performed by using the set.
The model checking has the above features, but has a problem in that a memory and a time required for calculation increases in an exponential manner with respect to the scale of the verification target. Therefore, in the model checking for the purpose of practically verifying a system and software, it is essential to increase the efficiency of the search.
For example, NPL 4 discloses DPOR (Dynamic Partial Order Reduction) which is a technique for pruning redundant searches from the perspective of verification in model checking of a multi-thread environment model.
When a state transition system of a model checking target is searched with the DPOR, a transition is initially made between states in one suitable path. Then, with the DPOR, a determination is made as to whether there exists a pair of transitions in which execution orders of each other affect an execution result in the transition series of the path. The pair of such transitions will be referred to as transitions having dependency. In a case where the transitions having dependency exist, for searching with making transition between the states in the path in which the execution order of the pair is switched, a backtrack location indicating the position where a new search is started is generated in that path. For example, a state immediately before one of the pair of transitions having dependency whichever is performed first is searched from the paths in which the search is executed previously, and this state is adopted as the backtrack location.
Then, when all the transitions having dependency is detected from the previous path, the search is resumed from the backtrack location at the rearmost on the path. This procedure is repeated until no more backtrack location is generated. Therefore, from among all the execution patterns of the verification target, only the path of which execution results is different can be searched. In other words, a search for a path of which verification result is not different, i.e., a search for a redundant path from the perspective of verification, can be pruned, so that the efficiency of the search can be enhanced.
NPL 5 discloses SDPOR which is a technique obtained by improving the DPOR. In the model checking, in general, when a state in which a search has been performed in the past (searched state) is attained again, a search after the state is terminated because the search is of course redundant. However, with the DPOR, easily terminating the search causes to affect an analysis of the transition having dependency on the path, and a correct result cannot be obtained. Therefore, with the DPOR, even if a searched state is attained, the search is not terminated and is continued.
The SDPOR is an improved DPOR that is configured to be able to terminate the search when the searched state is attained. With the SDPOR, transitions performed in the search in the past are managed with a graph, which is used for the analysis of the dependency. In the graph, a transition is associated with each node, and each directed edge represents an execution order of a transition performed in the search in the past. For example, it is assumed that a state immediately after a transition t1 performed in a search is s1, and when a transition t2 is performed further from s1, a directed edge is drawn from the node n1 associated with the transition t1 in the graph to a node n2 associated with the transition t2 (when the nodes n1 and n2 do not exist in the graph, the nodes n1 and n2 are generated).
With the SDPOR, when the state s2 searched in the past is reached, a transition that can be performed from the state s2 is investigated, and a node associated with the transition is searched from the graph, and further, all the nodes that can be reached by tracking the directed edge from the node are extracted. The transition associated with the node extracted above represents a transition that can be executed in a state transition of s2 or later. By analyzing the dependency by using these transitions and a transition on the current path, a backtrack location is generated. The advantage of the SDPOR is that, with these procedures, even when a search after the searched state is terminated, the dependency can be correctly analyzed, and the efficiency can be improved due to the termination of the search.
NPL 6 discloses DPOR-DS which is a technique obtained by correcting the DPOR for a model checking of a distributed-environment-model. For absorbing the difference in an environment of a model of a verification target, a method for generating the backtrack location is changed. A happens-before relation in the distributed-environment-model is defined separately from dependency with regard to a relation between transitions on an execution path, and this is used for determination of generation of the backtrack location. The happens-before relation is a relation in an execution order between transitions that are always satisfied in a certain model. For example, when a transition for transmitting and receiving a certain packet p is considered, the transition for transmitting the packet p always occurs before the transition for receiving the packet p. As described above, an order relation between the transitions that is always satisfied because of the causality in terms of the model is the happens-before relation.
With the DPOR-DS, even when not only the dependency but also presence and absence of the happens-before relation are analyzed with regard to the transition on the execution path, and the dependency exists between certain transitions, no backtrack location is generated in a case where the happens-before relation is satisfied. The characteristic of the DPOR-DS is that, with these procedures, even in the model checking of the distributed-environment-model, the search can be pruned in the same manner as in the DPOR.